($x$ after $e$)($t$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$s($e$.1;($e$.2)+1).$x$($t$ {-} 1)